2020-05-19 13:13:38 (GMT)
Hi all,
There is a set of problems similar to this one that no higher-order superposition (or paramodulation/resolution) prover can solve. I have been trying the whole day to solve this problem with pen and paper but I have no idea how to approach it.
If anyone sees where the trick lies, please let me know :slight_smile:
I think this problem might be intersting since it sheds some light on what resolution-based provers are doing wrong.
List of problems similar to this one: SEV243^5.p, SEV244^5.p, SEV244^6.p, SEV252^5.p.
2020-05-19 13:18:58 (GMT)
@Alexander Bentkamp : maybe this one is interesting for your calculus as well?
2020-05-19 14:26:56 (GMT)
Wow, this is a tough one. I think the => part of the equivalence is the hard one, right?
Let's formulate this problem in terms of sets. We have a map mapping sets to sets that preserves the subset relation. For the => direction we fix some and assume that . We have to show that there is a set such that and .
I think that choosing does the trick.
2020-05-19 15:20:34 (GMT)
BTW, are these for problems conceptually all the same? The formulations differ only in tiny details. For example, SEV243^5.p and SEV244^5.p differ only in ∀ x ∀ y vs ∀ y ∀ x at the beginning. Why?
2020-05-19 15:25:9 (GMT)
I can't think of a good reason except carelessness. Or testing HO provers that don't clausify.
2020-05-19 15:26:32 (GMT)
For CASC, Geoff does some obfuscation: he modifies existing problems automatically in ways that don't affect provability, so that provers can't (easily) recognize the problems and cheat. But surely it's a bad idea to do this in the library.
2020-05-19 15:51:49 (GMT)
Looking at the TPTP page, it appears as though Zipperposition can solve this with the help of E. Perhaps viewing the E proof would be instructive?
2020-05-19 16:2:51 (GMT)
This is by pure chance. The old version of Zipperposition accidentally did a superposition that would create something like K ( X K), and some good liftings were around and E proved it..
2020-05-19 16:3:4 (GMT)
A proof so ugly, I am happy we do not solve this problem anymore this way
2020-05-19 16:4:15 (GMT)
Alexander Bentkamp said:
BTW, are these for problems conceptually all the same? The formulations differ only in tiny details. For example,
SEV243^5.pandSEV244^5.pdiffer only in∀ x ∀ yvs∀ y ∀ xat the beginning. Why?
I know... it is quite strange..but if am right (@Jasmin Blanchette ) tableaux provers are sensitive to the smallest changes in the problem, such as the order of quantifiers
2020-05-19 16:4:20 (GMT)
so maybe they wanted to check this
2020-05-19 17:23:8 (GMT)
Maybe this will help?
2020-05-19 17:29:35 (GMT)
wow thanks a lot ... I have been looking for this paper for some time
2020-05-19 17:29:47 (GMT)
that is for this broken reference in
2020-05-19 18:57:15 (GMT)
Be aware that this is not implemented in Satallax, I believe.
2020-05-19 18:58:42 (GMT)
is that from pre-Vampire Voronkov?
2020-05-19 18:59:26 (GMT)
Editor != author
2020-05-19 19:0:8 (GMT)
Ah :face_palm: misread it indeed.
2020-05-19 19:8:41 (GMT)
Pre-Vampire Dracula?
2020-05-19 22:44:9 (GMT)
History point - the first version of Vampire was written in 1993 but was only named Vampire retrospectively when the second version was written in 1995.
2020-05-19 22:45:10 (GMT)
Oh and it seems originally there was an idea to name major versions after famous vampires but they didn't get any further than Dracula :)
2020-05-27 20:35:12 (GMT)
Lestat, Pandora, Marius... the Anne Rice novels would be a good source then.